0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxWeightedTrs
↳7 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedTrs
↳9 CompletionProof (UPPER BOUND(ID), 0 ms)
↳10 CpxTypedWeightedCompleteTrs
↳11 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 14 ms)
↳12 CpxRNTS
↳13 CompleteCoflocoProof (⇔, 29.7 s)
↳14 BOUNDS(1, n^3)
U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N))
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N))
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N))
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2))
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2))
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2))
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2))
U15(tt, V2) → U16(isNat(activate(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1))
U22(tt, V1) → U23(isNat(activate(V1)))
U23(tt) → tt
U31(tt, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2))
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2))
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2))
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2))
U35(tt, V2) → U36(isNat(activate(V2)))
U36(tt) → tt
U41(tt, V2) → U42(isNatKind(activate(V2)))
U42(tt) → tt
U51(tt) → tt
U61(tt, V2) → U62(isNatKind(activate(V2)))
U62(tt) → tt
U71(tt, N) → U72(isNatKind(activate(N)), activate(N))
U72(tt, N) → activate(N)
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N))
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N))
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N))
U84(tt, M, N) → s(plus(activate(N), activate(M)))
U91(tt, N) → U92(isNatKind(activate(N)))
U92(tt) → 0
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2))
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1))
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatKind(n__0) → tt
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2))
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1)))
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2))
plus(N, 0) → U71(isNat(N), N)
plus(N, s(M)) → U81(isNat(M), M, N)
x(N, 0) → U91(isNat(N), N)
x(N, s(M)) → U101(isNat(M), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
s(X) → n__s(X)
x(X1, X2) → n__x(X1, X2)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__s(X)) → s(activate(X))
activate(n__x(X1, X2)) → x(activate(X1), activate(X2))
activate(X) → X
U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N)) [1]
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N)) [1]
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N)) [1]
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2)) [1]
U35(tt, V2) → U36(isNat(activate(V2))) [1]
U36(tt) → tt [1]
U41(tt, V2) → U42(isNatKind(activate(V2))) [1]
U42(tt) → tt [1]
U51(tt) → tt [1]
U61(tt, V2) → U62(isNatKind(activate(V2))) [1]
U62(tt) → tt [1]
U71(tt, N) → U72(isNatKind(activate(N)), activate(N)) [1]
U72(tt, N) → activate(N) [1]
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N)) [1]
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N)) [1]
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N)) [1]
U84(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U91(tt, N) → U92(isNatKind(activate(N))) [1]
U92(tt) → 0 [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1))) [1]
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2)) [1]
plus(N, 0) → U71(isNat(N), N) [1]
plus(N, s(M)) → U81(isNat(M), M, N) [1]
x(N, 0) → U91(isNat(N), N) [1]
x(N, s(M)) → U101(isNat(M), M, N) [1]
0 → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0 [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__x(X1, X2)) → x(activate(X1), activate(X2)) [1]
activate(X) → X [1]
| 0 => 0' |
U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N)) [1]
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N)) [1]
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N)) [1]
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2)) [1]
U35(tt, V2) → U36(isNat(activate(V2))) [1]
U36(tt) → tt [1]
U41(tt, V2) → U42(isNatKind(activate(V2))) [1]
U42(tt) → tt [1]
U51(tt) → tt [1]
U61(tt, V2) → U62(isNatKind(activate(V2))) [1]
U62(tt) → tt [1]
U71(tt, N) → U72(isNatKind(activate(N)), activate(N)) [1]
U72(tt, N) → activate(N) [1]
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N)) [1]
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N)) [1]
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N)) [1]
U84(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U91(tt, N) → U92(isNatKind(activate(N))) [1]
U92(tt) → 0' [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1))) [1]
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2)) [1]
plus(N, 0') → U71(isNat(N), N) [1]
plus(N, s(M)) → U81(isNat(M), M, N) [1]
x(N, 0') → U91(isNat(N), N) [1]
x(N, s(M)) → U101(isNat(M), M, N) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__x(X1, X2)) → x(activate(X1), activate(X2)) [1]
activate(X) → X [1]
plus(N, 0') → U71(isNat(N), N) [1]
plus(N, s(M)) → U81(isNat(M), M, N) [1]
x(N, 0') → U91(isNat(N), N) [1]
x(N, s(M)) → U101(isNat(M), M, N) [1]
0' → n__0 [1]
s(X) → n__s(X) [1]
U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N)) [1]
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N)) [1]
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N)) [1]
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2)) [1]
U35(tt, V2) → U36(isNat(activate(V2))) [1]
U36(tt) → tt [1]
U41(tt, V2) → U42(isNatKind(activate(V2))) [1]
U42(tt) → tt [1]
U51(tt) → tt [1]
U61(tt, V2) → U62(isNatKind(activate(V2))) [1]
U62(tt) → tt [1]
U71(tt, N) → U72(isNatKind(activate(N)), activate(N)) [1]
U72(tt, N) → activate(N) [1]
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N)) [1]
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N)) [1]
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N)) [1]
U84(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U91(tt, N) → U92(isNatKind(activate(N))) [1]
U92(tt) → 0' [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1))) [1]
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2)) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__x(X1, X2)) → x(activate(X1), activate(X2)) [1]
activate(X) → X [1]
U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N)) [1]
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N)) [1]
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N)) [1]
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2)) [1]
U35(tt, V2) → U36(isNat(activate(V2))) [1]
U36(tt) → tt [1]
U41(tt, V2) → U42(isNatKind(activate(V2))) [1]
U42(tt) → tt [1]
U51(tt) → tt [1]
U61(tt, V2) → U62(isNatKind(activate(V2))) [1]
U62(tt) → tt [1]
U71(tt, N) → U72(isNatKind(activate(N)), activate(N)) [1]
U72(tt, N) → activate(N) [1]
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N)) [1]
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N)) [1]
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N)) [1]
U84(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U91(tt, N) → U92(isNatKind(activate(N))) [1]
U92(tt) → 0' [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1))) [1]
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2)) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__x(X1, X2)) → x(activate(X1), activate(X2)) [1]
activate(X) → X [1]
| U101 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x tt :: tt U102 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x isNatKind :: n__0:n__plus:n__s:n__x → tt activate :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U103 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x isNat :: n__0:n__plus:n__s:n__x → tt U104 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x plus :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x x :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U11 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U12 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U13 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U14 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U15 :: tt → n__0:n__plus:n__s:n__x → tt U16 :: tt → tt U21 :: tt → n__0:n__plus:n__s:n__x → tt U22 :: tt → n__0:n__plus:n__s:n__x → tt U23 :: tt → tt U31 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U32 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U33 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U34 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U35 :: tt → n__0:n__plus:n__s:n__x → tt U36 :: tt → tt U41 :: tt → n__0:n__plus:n__s:n__x → tt U42 :: tt → tt U51 :: tt → tt U61 :: tt → n__0:n__plus:n__s:n__x → tt U62 :: tt → tt U71 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U72 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U81 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U82 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U83 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U84 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x s :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U91 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U92 :: tt → n__0:n__plus:n__s:n__x 0' :: n__0:n__plus:n__s:n__x n__0 :: n__0:n__plus:n__s:n__x n__plus :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x n__s :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x n__x :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x |
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
tt => 0
n__0 => 0
0' -{ 1 }→ 0 :|:
U101(z, z', z'') -{ 1 }→ U102(isNatKind(activate(M)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U102(z, z', z'') -{ 1 }→ U103(isNat(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U103(z, z', z'') -{ 1 }→ U104(isNatKind(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U104(z, z', z'') -{ 1 }→ plus(x(activate(N), activate(M)), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U11(z, z', z'') -{ 1 }→ U12(isNatKind(activate(V1)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U12(z, z', z'') -{ 1 }→ U13(isNatKind(activate(V2)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U13(z, z', z'') -{ 1 }→ U14(isNatKind(activate(V2)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U14(z, z', z'') -{ 1 }→ U15(isNat(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U15(z, z') -{ 1 }→ U16(isNat(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U16(z) -{ 1 }→ 0 :|: z = 0
U21(z, z') -{ 1 }→ U22(isNatKind(activate(V1)), activate(V1)) :|: V1 >= 0, z = 0, z' = V1
U22(z, z') -{ 1 }→ U23(isNat(activate(V1))) :|: V1 >= 0, z = 0, z' = V1
U23(z) -{ 1 }→ 0 :|: z = 0
U31(z, z', z'') -{ 1 }→ U32(isNatKind(activate(V1)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U32(z, z', z'') -{ 1 }→ U33(isNatKind(activate(V2)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U33(z, z', z'') -{ 1 }→ U34(isNatKind(activate(V2)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U34(z, z', z'') -{ 1 }→ U35(isNat(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U35(z, z') -{ 1 }→ U36(isNat(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U36(z) -{ 1 }→ 0 :|: z = 0
U41(z, z') -{ 1 }→ U42(isNatKind(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U42(z) -{ 1 }→ 0 :|: z = 0
U51(z) -{ 1 }→ 0 :|: z = 0
U61(z, z') -{ 1 }→ U62(isNatKind(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U62(z) -{ 1 }→ 0 :|: z = 0
U71(z, z') -{ 1 }→ U72(isNatKind(activate(N)), activate(N)) :|: z' = N, z = 0, N >= 0
U72(z, z') -{ 1 }→ activate(N) :|: z' = N, z = 0, N >= 0
U81(z, z', z'') -{ 1 }→ U82(isNatKind(activate(M)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U82(z, z', z'') -{ 1 }→ U83(isNat(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U83(z, z', z'') -{ 1 }→ U84(isNatKind(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U84(z, z', z'') -{ 1 }→ s(plus(activate(N), activate(M))) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U91(z, z') -{ 1 }→ U92(isNatKind(activate(N))) :|: z' = N, z = 0, N >= 0
U92(z) -{ 1 }→ 0' :|: z = 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ x(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ s(activate(X)) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ plus(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ 0' :|: z = 0
isNat(z) -{ 1 }→ U31(isNatKind(activate(V1)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNat(z) -{ 1 }→ U21(isNatKind(activate(V1)), activate(V1)) :|: z = 1 + V1, V1 >= 0
isNat(z) -{ 1 }→ U11(isNatKind(activate(V1)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNat(z) -{ 1 }→ 0 :|: z = 0
isNatKind(z) -{ 1 }→ U61(isNatKind(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNatKind(z) -{ 1 }→ U51(isNatKind(activate(V1))) :|: z = 1 + V1, V1 >= 0
isNatKind(z) -{ 1 }→ U41(isNatKind(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNatKind(z) -{ 1 }→ 0 :|: z = 0
plus(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
x(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
| eq(start(V, V3, V4),0,[fun(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun1(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun2(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun3(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun4(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun5(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun6(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun7(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun8(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun9(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun10(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun11(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun12(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun13(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun14(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun15(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun16(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun17(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun18(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun19(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun20(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun21(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun22(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun23(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun24(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun25(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun26(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun27(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun28(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun29(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun30(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun31(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[isNat(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[isNatKind(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun32(Out)],[]). eq(start(V, V3, V4),0,[plus(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[s(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[x(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[activate(V, Out)],[V >= 0]). eq(fun(V, V3, V4, Out),1,[activate(M1, Ret00),isNatKind(Ret00, Ret0),activate(M1, Ret1),activate(N1, Ret2),fun1(Ret0, Ret1, Ret2, Ret)],[Out = Ret,V3 = M1,V = 0,V4 = N1,M1 >= 0,N1 >= 0]). eq(fun1(V, V3, V4, Out),1,[activate(N2, Ret001),isNat(Ret001, Ret01),activate(M2, Ret11),activate(N2, Ret21),fun2(Ret01, Ret11, Ret21, Ret3)],[Out = Ret3,V3 = M2,V = 0,V4 = N2,M2 >= 0,N2 >= 0]). eq(fun2(V, V3, V4, Out),1,[activate(N3, Ret002),isNatKind(Ret002, Ret02),activate(M3, Ret12),activate(N3, Ret22),fun3(Ret02, Ret12, Ret22, Ret4)],[Out = Ret4,V3 = M3,V = 0,V4 = N3,M3 >= 0,N3 >= 0]). eq(fun3(V, V3, V4, Out),1,[activate(N4, Ret003),activate(M4, Ret011),x(Ret003, Ret011, Ret03),activate(N4, Ret13),plus(Ret03, Ret13, Ret5)],[Out = Ret5,V3 = M4,V = 0,V4 = N4,M4 >= 0,N4 >= 0]). eq(fun4(V, V3, V4, Out),1,[activate(V11, Ret004),isNatKind(Ret004, Ret04),activate(V11, Ret14),activate(V21, Ret23),fun5(Ret04, Ret14, Ret23, Ret6)],[Out = Ret6,V11 >= 0,V21 >= 0,V = 0,V4 = V21,V3 = V11]). eq(fun5(V, V3, V4, Out),1,[activate(V22, Ret005),isNatKind(Ret005, Ret05),activate(V12, Ret15),activate(V22, Ret24),fun6(Ret05, Ret15, Ret24, Ret7)],[Out = Ret7,V12 >= 0,V22 >= 0,V = 0,V4 = V22,V3 = V12]). eq(fun6(V, V3, V4, Out),1,[activate(V23, Ret006),isNatKind(Ret006, Ret06),activate(V13, Ret16),activate(V23, Ret25),fun7(Ret06, Ret16, Ret25, Ret8)],[Out = Ret8,V13 >= 0,V23 >= 0,V = 0,V4 = V23,V3 = V13]). eq(fun7(V, V3, V4, Out),1,[activate(V14, Ret007),isNat(Ret007, Ret07),activate(V24, Ret17),fun8(Ret07, Ret17, Ret9)],[Out = Ret9,V14 >= 0,V24 >= 0,V = 0,V4 = V24,V3 = V14]). eq(fun8(V, V3, Out),1,[activate(V25, Ret008),isNat(Ret008, Ret08),fun9(Ret08, Ret10)],[Out = Ret10,V3 = V25,V25 >= 0,V = 0]). eq(fun9(V, Out),1,[],[Out = 0,V = 0]). eq(fun10(V, V3, Out),1,[activate(V15, Ret009),isNatKind(Ret009, Ret09),activate(V15, Ret18),fun11(Ret09, Ret18, Ret19)],[Out = Ret19,V15 >= 0,V = 0,V3 = V15]). eq(fun11(V, V3, Out),1,[activate(V16, Ret0010),isNat(Ret0010, Ret010),fun12(Ret010, Ret20)],[Out = Ret20,V16 >= 0,V = 0,V3 = V16]). eq(fun12(V, Out),1,[],[Out = 0,V = 0]). eq(fun13(V, V3, V4, Out),1,[activate(V17, Ret0011),isNatKind(Ret0011, Ret012),activate(V17, Ret110),activate(V26, Ret26),fun14(Ret012, Ret110, Ret26, Ret27)],[Out = Ret27,V17 >= 0,V26 >= 0,V = 0,V4 = V26,V3 = V17]). eq(fun14(V, V3, V4, Out),1,[activate(V27, Ret0012),isNatKind(Ret0012, Ret013),activate(V18, Ret111),activate(V27, Ret28),fun15(Ret013, Ret111, Ret28, Ret29)],[Out = Ret29,V18 >= 0,V27 >= 0,V = 0,V4 = V27,V3 = V18]). eq(fun15(V, V3, V4, Out),1,[activate(V28, Ret0013),isNatKind(Ret0013, Ret014),activate(V19, Ret112),activate(V28, Ret210),fun16(Ret014, Ret112, Ret210, Ret30)],[Out = Ret30,V19 >= 0,V28 >= 0,V = 0,V4 = V28,V3 = V19]). eq(fun16(V, V3, V4, Out),1,[activate(V110, Ret0014),isNat(Ret0014, Ret015),activate(V29, Ret113),fun17(Ret015, Ret113, Ret31)],[Out = Ret31,V110 >= 0,V29 >= 0,V = 0,V4 = V29,V3 = V110]). eq(fun17(V, V3, Out),1,[activate(V210, Ret0015),isNat(Ret0015, Ret016),fun18(Ret016, Ret32)],[Out = Ret32,V3 = V210,V210 >= 0,V = 0]). eq(fun18(V, Out),1,[],[Out = 0,V = 0]). eq(fun19(V, V3, Out),1,[activate(V211, Ret0016),isNatKind(Ret0016, Ret017),fun20(Ret017, Ret33)],[Out = Ret33,V3 = V211,V211 >= 0,V = 0]). eq(fun20(V, Out),1,[],[Out = 0,V = 0]). eq(fun21(V, Out),1,[],[Out = 0,V = 0]). eq(fun22(V, V3, Out),1,[activate(V212, Ret0017),isNatKind(Ret0017, Ret018),fun23(Ret018, Ret34)],[Out = Ret34,V3 = V212,V212 >= 0,V = 0]). eq(fun23(V, Out),1,[],[Out = 0,V = 0]). eq(fun24(V, V3, Out),1,[activate(N5, Ret0018),isNatKind(Ret0018, Ret019),activate(N5, Ret114),fun25(Ret019, Ret114, Ret35)],[Out = Ret35,V3 = N5,V = 0,N5 >= 0]). eq(fun25(V, V3, Out),1,[activate(N6, Ret36)],[Out = Ret36,V3 = N6,V = 0,N6 >= 0]). eq(fun26(V, V3, V4, Out),1,[activate(M5, Ret0019),isNatKind(Ret0019, Ret020),activate(M5, Ret115),activate(N7, Ret211),fun27(Ret020, Ret115, Ret211, Ret37)],[Out = Ret37,V3 = M5,V = 0,V4 = N7,M5 >= 0,N7 >= 0]). eq(fun27(V, V3, V4, Out),1,[activate(N8, Ret0020),isNat(Ret0020, Ret021),activate(M6, Ret116),activate(N8, Ret212),fun28(Ret021, Ret116, Ret212, Ret38)],[Out = Ret38,V3 = M6,V = 0,V4 = N8,M6 >= 0,N8 >= 0]). eq(fun28(V, V3, V4, Out),1,[activate(N9, Ret0021),isNatKind(Ret0021, Ret022),activate(M7, Ret117),activate(N9, Ret213),fun29(Ret022, Ret117, Ret213, Ret39)],[Out = Ret39,V3 = M7,V = 0,V4 = N9,M7 >= 0,N9 >= 0]). eq(fun29(V, V3, V4, Out),1,[activate(N10, Ret0022),activate(M8, Ret0110),plus(Ret0022, Ret0110, Ret023),s(Ret023, Ret40)],[Out = Ret40,V3 = M8,V = 0,V4 = N10,M8 >= 0,N10 >= 0]). eq(fun30(V, V3, Out),1,[activate(N11, Ret0023),isNatKind(Ret0023, Ret024),fun31(Ret024, Ret41)],[Out = Ret41,V3 = N11,V = 0,N11 >= 0]). eq(fun31(V, Out),1,[fun32(Ret42)],[Out = Ret42,V = 0]). eq(isNat(V, Out),1,[],[Out = 0,V = 0]). eq(isNat(V, Out),1,[activate(V111, Ret0024),isNatKind(Ret0024, Ret025),activate(V111, Ret118),activate(V213, Ret214),fun4(Ret025, Ret118, Ret214, Ret43)],[Out = Ret43,V111 >= 0,V213 >= 0,V = 1 + V111 + V213]). eq(isNat(V, Out),1,[activate(V112, Ret0025),isNatKind(Ret0025, Ret026),activate(V112, Ret119),fun10(Ret026, Ret119, Ret44)],[Out = Ret44,V = 1 + V112,V112 >= 0]). eq(isNat(V, Out),1,[activate(V113, Ret0026),isNatKind(Ret0026, Ret027),activate(V113, Ret120),activate(V214, Ret215),fun13(Ret027, Ret120, Ret215, Ret45)],[Out = Ret45,V113 >= 0,V214 >= 0,V = 1 + V113 + V214]). eq(isNatKind(V, Out),1,[],[Out = 0,V = 0]). eq(isNatKind(V, Out),1,[activate(V114, Ret0027),isNatKind(Ret0027, Ret028),activate(V215, Ret121),fun19(Ret028, Ret121, Ret46)],[Out = Ret46,V114 >= 0,V215 >= 0,V = 1 + V114 + V215]). eq(isNatKind(V, Out),1,[activate(V115, Ret0028),isNatKind(Ret0028, Ret029),fun21(Ret029, Ret47)],[Out = Ret47,V = 1 + V115,V115 >= 0]). eq(isNatKind(V, Out),1,[activate(V116, Ret0029),isNatKind(Ret0029, Ret030),activate(V216, Ret122),fun22(Ret030, Ret122, Ret48)],[Out = Ret48,V116 >= 0,V216 >= 0,V = 1 + V116 + V216]). eq(fun32(Out),1,[],[Out = 0]). eq(plus(V, V3, Out),1,[],[Out = 1 + X11 + X21,X11 >= 0,X21 >= 0,V = X11,V3 = X21]). eq(s(V, Out),1,[],[Out = 1 + X3,X3 >= 0,V = X3]). eq(x(V, V3, Out),1,[],[Out = 1 + X12 + X22,X12 >= 0,X22 >= 0,V = X12,V3 = X22]). eq(activate(V, Out),1,[fun32(Ret49)],[Out = Ret49,V = 0]). eq(activate(V, Out),1,[activate(X13, Ret031),activate(X23, Ret123),plus(Ret031, Ret123, Ret50)],[Out = Ret50,X13 >= 0,X23 >= 0,V = 1 + X13 + X23]). eq(activate(V, Out),1,[activate(X4, Ret032),s(Ret032, Ret51)],[Out = Ret51,V = 1 + X4,X4 >= 0]). eq(activate(V, Out),1,[activate(X14, Ret033),activate(X24, Ret124),x(Ret033, Ret124, Ret52)],[Out = Ret52,X14 >= 0,X24 >= 0,V = 1 + X14 + X24]). eq(activate(V, Out),1,[],[Out = X5,X5 >= 0,V = X5]). input_output_vars(fun(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun1(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun2(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun3(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun4(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun5(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun6(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun7(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun8(V,V3,Out),[V,V3],[Out]). input_output_vars(fun9(V,Out),[V],[Out]). input_output_vars(fun10(V,V3,Out),[V,V3],[Out]). input_output_vars(fun11(V,V3,Out),[V,V3],[Out]). input_output_vars(fun12(V,Out),[V],[Out]). input_output_vars(fun13(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun14(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun15(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun16(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun17(V,V3,Out),[V,V3],[Out]). input_output_vars(fun18(V,Out),[V],[Out]). input_output_vars(fun19(V,V3,Out),[V,V3],[Out]). input_output_vars(fun20(V,Out),[V],[Out]). input_output_vars(fun21(V,Out),[V],[Out]). input_output_vars(fun22(V,V3,Out),[V,V3],[Out]). input_output_vars(fun23(V,Out),[V],[Out]). input_output_vars(fun24(V,V3,Out),[V,V3],[Out]). input_output_vars(fun25(V,V3,Out),[V,V3],[Out]). input_output_vars(fun26(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun27(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun28(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun29(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun30(V,V3,Out),[V,V3],[Out]). input_output_vars(fun31(V,Out),[V],[Out]). input_output_vars(isNat(V,Out),[V],[Out]). input_output_vars(isNatKind(V,Out),[V],[Out]). input_output_vars(fun32(Out),[],[Out]). input_output_vars(plus(V,V3,Out),[V,V3],[Out]). input_output_vars(s(V,Out),[V],[Out]). input_output_vars(x(V,V3,Out),[V,V3],[Out]). input_output_vars(activate(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [fun32/1]
1. non_recursive : [plus/3]
2. non_recursive : [s/2]
3. non_recursive : [x/3]
4. recursive [non_tail,multiple] : [activate/2]
5. non_recursive : [fun3/4]
6. non_recursive : [fun20/2]
7. non_recursive : [fun21/2]
8. non_recursive : [fun23/2]
9. recursive [non_tail,multiple] : [fun19/3,fun22/3,isNatKind/2]
10. non_recursive : [fun2/4]
11. non_recursive : [fun12/2]
12. non_recursive : [fun18/2]
13. non_recursive : [fun9/2]
14. recursive [non_tail,multiple] : [fun10/3,fun11/3,fun13/4,fun14/4,fun15/4,fun16/4,fun17/3,fun4/4,fun5/4,fun6/4,fun7/4,fun8/3,isNat/2]
15. non_recursive : [fun1/4]
16. non_recursive : [fun/4]
17. non_recursive : [fun25/3]
18. non_recursive : [fun24/3]
19. non_recursive : [fun29/4]
20. non_recursive : [fun28/4]
21. non_recursive : [fun27/4]
22. non_recursive : [fun26/4]
23. non_recursive : [fun31/2]
24. non_recursive : [fun30/3]
25. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is completely evaluated into other SCCs
1. SCC is completely evaluated into other SCCs
2. SCC is completely evaluated into other SCCs
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into activate/2
5. SCC is partially evaluated into fun3/4
6. SCC is completely evaluated into other SCCs
7. SCC is completely evaluated into other SCCs
8. SCC is completely evaluated into other SCCs
9. SCC is partially evaluated into isNatKind/2
10. SCC is partially evaluated into fun2/4
11. SCC is completely evaluated into other SCCs
12. SCC is completely evaluated into other SCCs
13. SCC is completely evaluated into other SCCs
14. SCC is partially evaluated into isNat/2
15. SCC is partially evaluated into fun1/4
16. SCC is partially evaluated into fun/4
17. SCC is completely evaluated into other SCCs
18. SCC is partially evaluated into fun24/3
19. SCC is partially evaluated into fun29/4
20. SCC is partially evaluated into fun28/4
21. SCC is partially evaluated into fun27/4
22. SCC is partially evaluated into fun26/4
23. SCC is completely evaluated into other SCCs
24. SCC is partially evaluated into fun30/3
25. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations activate/2
* CE 25 is refined into CE [45]
* CE 28 is refined into CE [46]
* CE 27 is refined into CE [47]
* CE 26 is refined into CE [48]
### Cost equations --> "Loop" of activate/2
* CEs [48] --> Loop 21
* CEs [47] --> Loop 22
* CEs [45,46] --> Loop 23
### Ranking functions of CR activate(V,Out)
* RF of phase [21,22]: [V]
#### Partial ranking functions of CR activate(V,Out)
* Partial RF of phase [21,22]:
- RF of loop [21:1,21:2,22:1]:
V
### Specialization of cost equations fun3/4
* CE 38 is refined into CE [49]
### Cost equations --> "Loop" of fun3/4
* CEs [49] --> Loop 24
### Ranking functions of CR fun3(V,V3,V4,Out)
#### Partial ranking functions of CR fun3(V,V3,V4,Out)
### Specialization of cost equations isNatKind/2
* CE 31 is refined into CE [50]
* CE 30 is refined into CE [51]
* CE 29 is refined into CE [52]
### Cost equations --> "Loop" of isNatKind/2
* CEs [52] --> Loop 25
* CEs [51] --> Loop 26
* CEs [50] --> Loop 27
### Ranking functions of CR isNatKind(V,Out)
* RF of phase [25,27]: [V]
#### Partial ranking functions of CR isNatKind(V,Out)
* Partial RF of phase [25,27]:
- RF of loop [25:1,25:2,27:1]:
V
### Specialization of cost equations fun2/4
* CE 37 is refined into CE [53,54]
### Cost equations --> "Loop" of fun2/4
* CEs [54] --> Loop 28
* CEs [53] --> Loop 29
### Ranking functions of CR fun2(V,V3,V4,Out)
#### Partial ranking functions of CR fun2(V,V3,V4,Out)
### Specialization of cost equations isNat/2
* CE 34 is refined into CE [55]
* CE 33 is refined into CE [56,57]
* CE 32 is refined into CE [58,59,60,61]
### Cost equations --> "Loop" of isNat/2
* CEs [61] --> Loop 30
* CEs [60] --> Loop 31
* CEs [59] --> Loop 32
* CEs [58] --> Loop 33
* CEs [57] --> Loop 34
* CEs [56] --> Loop 35
* CEs [55] --> Loop 36
### Ranking functions of CR isNat(V,Out)
* RF of phase [30,31,32,34]: [V-1]
#### Partial ranking functions of CR isNat(V,Out)
* Partial RF of phase [30,31,32,34]:
- RF of loop [30:1,30:2]:
V/2-1
- RF of loop [31:1,31:2,32:1,32:2,34:1]:
V-1
### Specialization of cost equations fun1/4
* CE 36 is refined into CE [62,63,64]
### Cost equations --> "Loop" of fun1/4
* CEs [64] --> Loop 37
* CEs [63] --> Loop 38
* CEs [62] --> Loop 39
### Ranking functions of CR fun1(V,V3,V4,Out)
#### Partial ranking functions of CR fun1(V,V3,V4,Out)
### Specialization of cost equations fun/4
* CE 35 is refined into CE [65,66,67,68,69,70]
### Cost equations --> "Loop" of fun/4
* CEs [70] --> Loop 40
* CEs [69] --> Loop 41
* CEs [68] --> Loop 42
* CEs [67] --> Loop 43
* CEs [66] --> Loop 44
* CEs [65] --> Loop 45
### Ranking functions of CR fun(V,V3,V4,Out)
#### Partial ranking functions of CR fun(V,V3,V4,Out)
### Specialization of cost equations fun24/3
* CE 39 is refined into CE [71,72]
### Cost equations --> "Loop" of fun24/3
* CEs [72] --> Loop 46
* CEs [71] --> Loop 47
### Ranking functions of CR fun24(V,V3,Out)
#### Partial ranking functions of CR fun24(V,V3,Out)
### Specialization of cost equations fun29/4
* CE 43 is refined into CE [73]
### Cost equations --> "Loop" of fun29/4
* CEs [73] --> Loop 48
### Ranking functions of CR fun29(V,V3,V4,Out)
#### Partial ranking functions of CR fun29(V,V3,V4,Out)
### Specialization of cost equations fun28/4
* CE 42 is refined into CE [74,75]
### Cost equations --> "Loop" of fun28/4
* CEs [75] --> Loop 49
* CEs [74] --> Loop 50
### Ranking functions of CR fun28(V,V3,V4,Out)
#### Partial ranking functions of CR fun28(V,V3,V4,Out)
### Specialization of cost equations fun27/4
* CE 41 is refined into CE [76,77,78]
### Cost equations --> "Loop" of fun27/4
* CEs [78] --> Loop 51
* CEs [77] --> Loop 52
* CEs [76] --> Loop 53
### Ranking functions of CR fun27(V,V3,V4,Out)
#### Partial ranking functions of CR fun27(V,V3,V4,Out)
### Specialization of cost equations fun26/4
* CE 40 is refined into CE [79,80,81,82,83,84]
### Cost equations --> "Loop" of fun26/4
* CEs [84] --> Loop 54
* CEs [83] --> Loop 55
* CEs [82] --> Loop 56
* CEs [81] --> Loop 57
* CEs [80] --> Loop 58
* CEs [79] --> Loop 59
### Ranking functions of CR fun26(V,V3,V4,Out)
#### Partial ranking functions of CR fun26(V,V3,V4,Out)
### Specialization of cost equations fun30/3
* CE 44 is refined into CE [85,86]
### Cost equations --> "Loop" of fun30/3
* CEs [86] --> Loop 60
* CEs [85] --> Loop 61
### Ranking functions of CR fun30(V,V3,Out)
#### Partial ranking functions of CR fun30(V,V3,Out)
### Specialization of cost equations start/3
* CE 2 is refined into CE [87,88,89,90,91,92,93,94,95]
* CE 3 is refined into CE [96,97,98,99,100,101,102,103,104]
* CE 4 is refined into CE [105,106,107,108,109,110,111,112,113]
* CE 5 is refined into CE [114,115,116,117,118,119,120,121,122]
* CE 6 is refined into CE [123,124,125]
* CE 7 is refined into CE [126,127,128]
* CE 8 is refined into CE [129,130]
* CE 9 is refined into CE [131,132,133,134,135,136]
* CE 10 is refined into CE [137,138,139]
* CE 11 is refined into CE [140,141]
* CE 12 is refined into CE [142]
* CE 13 is refined into CE [143]
* CE 14 is refined into CE [144,145]
* CE 15 is refined into CE [146]
* CE 16 is refined into CE [147,148,149,150,151,152]
* CE 17 is refined into CE [153,154,155]
* CE 18 is refined into CE [156,157]
* CE 19 is refined into CE [158]
* CE 20 is refined into CE [159,160]
* CE 21 is refined into CE [161]
* CE 22 is refined into CE [162,163,164]
* CE 23 is refined into CE [165,166]
* CE 24 is refined into CE [167]
### Cost equations --> "Loop" of start/3
* CEs [87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167] --> Loop 62
### Ranking functions of CR start(V,V3,V4)
#### Partial ranking functions of CR start(V,V3,V4)
Computing Bounds
=====================================
#### Cost of chains of activate(V,Out):
* Chain [23]: 2
with precondition: [V=Out,V>=0]
* Chain [multiple([21,22],[[23]])]: 4*it(21)+2*it([23])+0
Such that:it([23]) =< V+1
aux(1) =< V
it(21) =< aux(1)
with precondition: [V=Out,V>=1]
#### Cost of chains of fun3(V,V3,V4,Out):
* Chain [24]: 4*s(5)+8*s(6)+2*s(8)+4*s(9)+9
Such that:s(7) =< V3
s(8) =< V3+1
aux(2) =< V4
aux(3) =< V4+1
s(5) =< aux(3)
s(6) =< aux(2)
s(9) =< s(7)
with precondition: [V=0,V3+2*V4+2=Out,V3>=0,V4>=0]
#### Cost of chains of isNatKind(V,Out):
* Chain [26]: 1
with precondition: [V=0,Out=0]
* Chain [multiple([25,27],[[26]])]: 13*it(25)+1*it([26])+2*s(34)+4*s(35)+10*s(36)+8*s(37)+0
Such that:it([26]) =< V+1
aux(12) =< V
it(25) =< aux(12)
aux(8) =< aux(12)+1
aux(9) =< aux(12)
s(38) =< it(25)*aux(12)
s(40) =< it(25)*aux(8)
s(39) =< it(25)*aux(9)
s(34) =< it(25)*aux(8)
s(36) =< s(40)
s(37) =< s(39)
s(35) =< s(38)
with precondition: [Out=0,V>=1]
#### Cost of chains of fun2(V,V3,V4,Out):
* Chain [29]: 8*s(44)+4*s(47)+8*s(48)+17
Such that:aux(14) =< 1
aux(15) =< V3
aux(16) =< V3+1
s(44) =< aux(14)
s(47) =< aux(16)
s(48) =< aux(15)
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [28]: 9*s(60)+29*s(61)+2*s(70)+10*s(71)+8*s(72)+4*s(73)+4*s(75)+8*s(76)+16
Such that:aux(17) =< V3
aux(18) =< V3+1
aux(19) =< V4
aux(20) =< V4+1
s(75) =< aux(18)
s(60) =< aux(20)
s(61) =< aux(19)
s(76) =< aux(17)
s(65) =< aux(19)+1
s(66) =< aux(19)
s(67) =< s(61)*aux(19)
s(68) =< s(61)*s(65)
s(69) =< s(61)*s(66)
s(70) =< s(61)*s(65)
s(71) =< s(68)
s(72) =< s(69)
s(73) =< s(67)
with precondition: [V=0,V3+2*V4+2=Out,V3>=0,V4>=1]
#### Cost of chains of isNat(V,Out):
* Chain [36]: 1
with precondition: [V=0,Out=0]
* Chain [35,36]: 10*s(88)+17
Such that:aux(22) =< 1
s(88) =< aux(22)
with precondition: [V=1,Out=0]
* Chain [multiple(33,[[36]])]: 30*s(103)+43
Such that:aux(24) =< 1
s(103) =< aux(24)
with precondition: [V=1,Out=0]
* Chain [multiple([30,31,32,34],[[36],[35,36],[multiple(33,[[36]])]])]: 37*it(30)+78*it(31)+14*it(34)+57*it([35,36])+1*it([36])+43*it([multiple(33,[[36]])])+88*s(484)+4*s(485)+20*s(486)+16*s(487)+8*s(488)+58*s(490)+4*s(491)+20*s(492)+16*s(493)+8*s(494)+34*s(504)+112*s(505)+8*s(506)+40*s(507)+32*s(508)+16*s(509)+30*s(510)+12*s(530)+46*s(531)+4*s(532)+20*s(533)+16*s(534)+8*s(535)+0
Such that:aux(56) =< V
aux(57) =< V+1
aux(58) =< V/2
aux(59) =< V/2+1/2
aux(60) =< 2/3*V
it(34) =< aux(56)
it([36]) =< aux(57)
it([multiple(33,[[36]])]) =< aux(57)
it(30) =< aux(58)
it([35,36]) =< aux(59)
it([multiple(33,[[36]])]) =< aux(59)
aux(43) =< aux(60)
it(31) =< aux(60)
aux(45) =< aux(56)+2
aux(39) =< aux(56)+1
aux(40) =< aux(56)
it(34) =< it([36])+aux(56)
aux(43) =< it([36])* (1/3)+aux(60)
it(31) =< it([36])* (1/3)+aux(60)
it(30) =< it([36])* (1/2)+aux(58)
it(31) =< it([36])* (1/2)+aux(58)
s(540) =< it(34)*aux(45)
s(539) =< it(34)*aux(39)
s(515) =< it(31)*aux(45)
s(514) =< it(31)*aux(39)
s(502) =< it(30)*aux(39)
s(501) =< it(30)*aux(40)
s(530) =< s(540)
s(531) =< s(539)
s(255) =< aux(39)+1
s(256) =< aux(39)
s(536) =< s(531)*aux(39)
s(538) =< s(531)*s(255)
s(537) =< s(531)*s(256)
s(532) =< s(531)*s(255)
s(533) =< s(538)
s(534) =< s(537)
s(535) =< s(536)
s(510) =< aux(43)
s(504) =< s(515)
s(505) =< s(514)
s(511) =< s(505)*aux(39)
s(513) =< s(505)*s(255)
s(512) =< s(505)*s(256)
s(506) =< s(505)*s(255)
s(507) =< s(513)
s(508) =< s(512)
s(509) =< s(511)
s(484) =< s(502)
s(490) =< s(501)
s(498) =< s(490)*aux(56)
s(500) =< s(490)*aux(39)
s(499) =< s(490)*aux(40)
s(491) =< s(490)*aux(39)
s(492) =< s(500)
s(493) =< s(499)
s(494) =< s(498)
s(495) =< s(484)*aux(39)
s(497) =< s(484)*s(255)
s(496) =< s(484)*s(256)
s(485) =< s(484)*s(255)
s(486) =< s(497)
s(487) =< s(496)
s(488) =< s(495)
with precondition: [Out=0,V>=2]
#### Cost of chains of fun1(V,V3,V4,Out):
* Chain [39]: 12*s(550)+6*s(553)+12*s(554)+25
Such that:aux(63) =< 1
aux(64) =< V3
aux(65) =< V3+1
s(550) =< aux(63)
s(553) =< aux(65)
s(554) =< aux(64)
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [38]: 13*s(565)+37*s(566)+6*s(568)+12*s(569)+2*s(586)+10*s(587)+8*s(588)+4*s(589)+106
Such that:aux(66) =< 1
aux(67) =< 2
aux(68) =< V3
aux(69) =< V3+1
s(565) =< aux(67)
s(568) =< aux(69)
s(566) =< aux(66)
s(569) =< aux(68)
s(581) =< aux(66)+1
s(582) =< aux(66)
s(583) =< s(566)*aux(66)
s(584) =< s(566)*s(581)
s(585) =< s(566)*s(582)
s(586) =< s(566)*s(581)
s(587) =< s(584)
s(588) =< s(585)
s(589) =< s(583)
with precondition: [V=0,V4=1,V3+4=Out,V3>=0]
* Chain [37]: 14*s(591)+37*s(592)+14*s(598)+43*s(600)+37*s(601)+57*s(602)+78*s(604)+12*s(614)+46*s(615)+4*s(621)+20*s(622)+16*s(623)+8*s(624)+30*s(625)+34*s(626)+112*s(627)+8*s(631)+40*s(632)+32*s(633)+16*s(634)+88*s(635)+58*s(636)+4*s(640)+20*s(641)+16*s(642)+8*s(643)+4*s(647)+20*s(648)+16*s(649)+8*s(650)+6*s(652)+12*s(653)+2*s(670)+10*s(671)+8*s(672)+4*s(673)+23
Such that:s(595) =< V4/2
s(596) =< V4/2+1/2
s(597) =< 2/3*V4
aux(70) =< V3
aux(71) =< V3+1
aux(72) =< V4
aux(73) =< V4+1
s(652) =< aux(71)
s(591) =< aux(73)
s(592) =< aux(72)
s(653) =< aux(70)
s(606) =< aux(72)+1
s(607) =< aux(72)
s(667) =< s(592)*aux(72)
s(668) =< s(592)*s(606)
s(669) =< s(592)*s(607)
s(670) =< s(592)*s(606)
s(671) =< s(668)
s(672) =< s(669)
s(673) =< s(667)
s(598) =< aux(72)
s(600) =< aux(73)
s(601) =< s(595)
s(602) =< s(596)
s(600) =< s(596)
s(603) =< s(597)
s(604) =< s(597)
s(605) =< aux(72)+2
s(598) =< s(591)+aux(72)
s(603) =< s(591)* (1/3)+s(597)
s(604) =< s(591)* (1/3)+s(597)
s(601) =< s(591)* (1/2)+s(595)
s(604) =< s(591)* (1/2)+s(595)
s(608) =< s(598)*s(605)
s(609) =< s(598)*s(606)
s(610) =< s(604)*s(605)
s(611) =< s(604)*s(606)
s(612) =< s(601)*s(606)
s(613) =< s(601)*s(607)
s(614) =< s(608)
s(615) =< s(609)
s(616) =< s(606)+1
s(617) =< s(606)
s(618) =< s(615)*s(606)
s(619) =< s(615)*s(616)
s(620) =< s(615)*s(617)
s(621) =< s(615)*s(616)
s(622) =< s(619)
s(623) =< s(620)
s(624) =< s(618)
s(625) =< s(603)
s(626) =< s(610)
s(627) =< s(611)
s(628) =< s(627)*s(606)
s(629) =< s(627)*s(616)
s(630) =< s(627)*s(617)
s(631) =< s(627)*s(616)
s(632) =< s(629)
s(633) =< s(630)
s(634) =< s(628)
s(635) =< s(612)
s(636) =< s(613)
s(637) =< s(636)*aux(72)
s(638) =< s(636)*s(606)
s(639) =< s(636)*s(607)
s(640) =< s(636)*s(606)
s(641) =< s(638)
s(642) =< s(639)
s(643) =< s(637)
s(644) =< s(635)*s(606)
s(645) =< s(635)*s(616)
s(646) =< s(635)*s(617)
s(647) =< s(635)*s(616)
s(648) =< s(645)
s(649) =< s(646)
s(650) =< s(644)
with precondition: [V=0,V3+2*V4+2=Out,V3>=0,V4>=2]
#### Cost of chains of fun(V,V3,V4,Out):
* Chain [45]: 24*s(675)+33
Such that:aux(75) =< 1
s(675) =< aux(75)
with precondition: [V=0,V3=0,V4=0,Out=2]
* Chain [44]: 51*s(690)+15*s(696)+2*s(711)+10*s(712)+8*s(713)+4*s(714)+114
Such that:aux(77) =< 1
aux(78) =< 2
s(690) =< aux(77)
s(696) =< aux(78)
s(706) =< aux(77)+1
s(707) =< aux(77)
s(708) =< s(690)*aux(77)
s(709) =< s(690)*s(706)
s(710) =< s(690)*s(707)
s(711) =< s(690)*s(706)
s(712) =< s(709)
s(713) =< s(710)
s(714) =< s(708)
with precondition: [V=0,V3=0,V4=1,Out=4]
* Chain [43]: 10*s(716)+16*s(722)+41*s(723)+2*s(740)+10*s(741)+8*s(742)+4*s(743)+14*s(744)+43*s(745)+37*s(746)+57*s(747)+78*s(749)+12*s(757)+46*s(758)+4*s(764)+20*s(765)+16*s(766)+8*s(767)+30*s(768)+34*s(769)+112*s(770)+8*s(774)+40*s(775)+32*s(776)+16*s(777)+88*s(778)+58*s(779)+4*s(783)+20*s(784)+16*s(785)+8*s(786)+4*s(790)+20*s(791)+16*s(792)+8*s(793)+31
Such that:s(724) =< V4/2
s(725) =< V4/2+1/2
s(726) =< 2/3*V4
aux(80) =< 1
aux(81) =< V4
aux(82) =< V4+1
s(716) =< aux(80)
s(722) =< aux(82)
s(723) =< aux(81)
s(735) =< aux(81)+1
s(736) =< aux(81)
s(737) =< s(723)*aux(81)
s(738) =< s(723)*s(735)
s(739) =< s(723)*s(736)
s(740) =< s(723)*s(735)
s(741) =< s(738)
s(742) =< s(739)
s(743) =< s(737)
s(744) =< aux(81)
s(745) =< aux(82)
s(746) =< s(724)
s(747) =< s(725)
s(745) =< s(725)
s(748) =< s(726)
s(749) =< s(726)
s(750) =< aux(81)+2
s(744) =< s(722)+aux(81)
s(748) =< s(722)* (1/3)+s(726)
s(749) =< s(722)* (1/3)+s(726)
s(746) =< s(722)* (1/2)+s(724)
s(749) =< s(722)* (1/2)+s(724)
s(751) =< s(744)*s(750)
s(752) =< s(744)*s(735)
s(753) =< s(749)*s(750)
s(754) =< s(749)*s(735)
s(755) =< s(746)*s(735)
s(756) =< s(746)*s(736)
s(757) =< s(751)
s(758) =< s(752)
s(759) =< s(735)+1
s(760) =< s(735)
s(761) =< s(758)*s(735)
s(762) =< s(758)*s(759)
s(763) =< s(758)*s(760)
s(764) =< s(758)*s(759)
s(765) =< s(762)
s(766) =< s(763)
s(767) =< s(761)
s(768) =< s(748)
s(769) =< s(753)
s(770) =< s(754)
s(771) =< s(770)*s(735)
s(772) =< s(770)*s(759)
s(773) =< s(770)*s(760)
s(774) =< s(770)*s(759)
s(775) =< s(772)
s(776) =< s(773)
s(777) =< s(771)
s(778) =< s(755)
s(779) =< s(756)
s(780) =< s(779)*aux(81)
s(781) =< s(779)*s(735)
s(782) =< s(779)*s(736)
s(783) =< s(779)*s(735)
s(784) =< s(781)
s(785) =< s(782)
s(786) =< s(780)
s(787) =< s(778)*s(735)
s(788) =< s(778)*s(759)
s(789) =< s(778)*s(760)
s(790) =< s(778)*s(759)
s(791) =< s(788)
s(792) =< s(789)
s(793) =< s(787)
with precondition: [V=0,V3=0,2*V4+2=Out,V4>=2]
* Chain [42]: 11*s(795)+33*s(796)+2*s(805)+10*s(806)+8*s(807)+4*s(808)+14*s(813)+32
Such that:aux(83) =< 1
aux(84) =< V3
aux(85) =< V3+1
s(813) =< aux(83)
s(795) =< aux(85)
s(796) =< aux(84)
s(800) =< aux(84)+1
s(801) =< aux(84)
s(802) =< s(796)*aux(84)
s(803) =< s(796)*s(800)
s(804) =< s(796)*s(801)
s(805) =< s(796)*s(800)
s(806) =< s(803)
s(807) =< s(804)
s(808) =< s(802)
with precondition: [V=0,V4=0,V3+2=Out,V3>=1]
* Chain [41]: 11*s(822)+33*s(823)+2*s(832)+10*s(833)+8*s(834)+4*s(835)+15*s(840)+41*s(841)+2*s(855)+10*s(856)+8*s(857)+4*s(858)+113
Such that:aux(86) =< 1
aux(87) =< 2
aux(88) =< V3
aux(89) =< V3+1
s(840) =< aux(87)
s(822) =< aux(89)
s(841) =< aux(86)
s(823) =< aux(88)
s(850) =< aux(86)+1
s(851) =< aux(86)
s(852) =< s(841)*aux(86)
s(853) =< s(841)*s(850)
s(854) =< s(841)*s(851)
s(855) =< s(841)*s(850)
s(856) =< s(853)
s(857) =< s(854)
s(858) =< s(852)
s(827) =< aux(88)+1
s(828) =< aux(88)
s(829) =< s(823)*aux(88)
s(830) =< s(823)*s(827)
s(831) =< s(823)*s(828)
s(832) =< s(823)*s(827)
s(833) =< s(830)
s(834) =< s(831)
s(835) =< s(829)
with precondition: [V=0,V4=1,V3+4=Out,V3>=1]
* Chain [40]: 11*s(860)+33*s(861)+2*s(870)+10*s(871)+8*s(872)+4*s(873)+16*s(878)+41*s(879)+2*s(896)+10*s(897)+8*s(898)+4*s(899)+14*s(900)+43*s(901)+37*s(902)+57*s(903)+78*s(905)+12*s(913)+46*s(914)+4*s(920)+20*s(921)+16*s(922)+8*s(923)+30*s(924)+34*s(925)+112*s(926)+8*s(930)+40*s(931)+32*s(932)+16*s(933)+88*s(934)+58*s(935)+4*s(939)+20*s(940)+16*s(941)+8*s(942)+4*s(946)+20*s(947)+16*s(948)+8*s(949)+30
Such that:s(880) =< V4/2
s(881) =< V4/2+1/2
s(882) =< 2/3*V4
aux(90) =< V3
aux(91) =< V3+1
aux(92) =< V4
aux(93) =< V4+1
s(860) =< aux(91)
s(878) =< aux(93)
s(879) =< aux(92)
s(861) =< aux(90)
s(891) =< aux(92)+1
s(892) =< aux(92)
s(893) =< s(879)*aux(92)
s(894) =< s(879)*s(891)
s(895) =< s(879)*s(892)
s(896) =< s(879)*s(891)
s(897) =< s(894)
s(898) =< s(895)
s(899) =< s(893)
s(900) =< aux(92)
s(901) =< aux(93)
s(902) =< s(880)
s(903) =< s(881)
s(901) =< s(881)
s(904) =< s(882)
s(905) =< s(882)
s(906) =< aux(92)+2
s(900) =< s(878)+aux(92)
s(904) =< s(878)* (1/3)+s(882)
s(905) =< s(878)* (1/3)+s(882)
s(902) =< s(878)* (1/2)+s(880)
s(905) =< s(878)* (1/2)+s(880)
s(907) =< s(900)*s(906)
s(908) =< s(900)*s(891)
s(909) =< s(905)*s(906)
s(910) =< s(905)*s(891)
s(911) =< s(902)*s(891)
s(912) =< s(902)*s(892)
s(913) =< s(907)
s(914) =< s(908)
s(915) =< s(891)+1
s(916) =< s(891)
s(917) =< s(914)*s(891)
s(918) =< s(914)*s(915)
s(919) =< s(914)*s(916)
s(920) =< s(914)*s(915)
s(921) =< s(918)
s(922) =< s(919)
s(923) =< s(917)
s(924) =< s(904)
s(925) =< s(909)
s(926) =< s(910)
s(927) =< s(926)*s(891)
s(928) =< s(926)*s(915)
s(929) =< s(926)*s(916)
s(930) =< s(926)*s(915)
s(931) =< s(928)
s(932) =< s(929)
s(933) =< s(927)
s(934) =< s(911)
s(935) =< s(912)
s(936) =< s(935)*aux(92)
s(937) =< s(935)*s(891)
s(938) =< s(935)*s(892)
s(939) =< s(935)*s(891)
s(940) =< s(937)
s(941) =< s(938)
s(942) =< s(936)
s(943) =< s(934)*s(891)
s(944) =< s(934)*s(915)
s(945) =< s(934)*s(916)
s(946) =< s(934)*s(915)
s(947) =< s(944)
s(948) =< s(945)
s(949) =< s(943)
s(865) =< aux(90)+1
s(866) =< aux(90)
s(867) =< s(861)*aux(90)
s(868) =< s(861)*s(865)
s(869) =< s(861)*s(866)
s(870) =< s(861)*s(865)
s(871) =< s(868)
s(872) =< s(869)
s(873) =< s(867)
with precondition: [V=0,V3+2*V4+2=Out,V3>=1,V4>=2]
#### Cost of chains of fun24(V,V3,Out):
* Chain [47]: 6*s(951)+9
Such that:aux(95) =< 1
s(951) =< aux(95)
with precondition: [V=0,V3=0,Out=0]
* Chain [46]: 7*s(960)+25*s(961)+2*s(970)+10*s(971)+8*s(972)+4*s(973)+8
Such that:aux(96) =< V3
aux(97) =< V3+1
s(960) =< aux(97)
s(961) =< aux(96)
s(965) =< aux(96)+1
s(966) =< aux(96)
s(967) =< s(961)*aux(96)
s(968) =< s(961)*s(965)
s(969) =< s(961)*s(966)
s(970) =< s(961)*s(965)
s(971) =< s(968)
s(972) =< s(969)
s(973) =< s(967)
with precondition: [V=0,V3=Out,V3>=1]
#### Cost of chains of fun29(V,V3,V4,Out):
* Chain [48]: 2*s(981)+4*s(982)+2*s(984)+4*s(985)+7
Such that:s(983) =< V3
s(984) =< V3+1
s(980) =< V4
s(981) =< V4+1
s(985) =< s(983)
s(982) =< s(980)
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=0]
#### Cost of chains of fun28(V,V3,V4,Out):
* Chain [50]: 6*s(987)+4*s(990)+8*s(991)+15
Such that:aux(99) =< 1
aux(100) =< V3
aux(101) =< V3+1
s(987) =< aux(99)
s(990) =< aux(101)
s(991) =< aux(100)
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [49]: 7*s(1002)+25*s(1003)+2*s(1012)+10*s(1013)+8*s(1014)+4*s(1015)+4*s(1017)+8*s(1018)+14
Such that:aux(102) =< V3
aux(103) =< V3+1
aux(104) =< V4
aux(105) =< V4+1
s(1017) =< aux(103)
s(1002) =< aux(105)
s(1018) =< aux(102)
s(1003) =< aux(104)
s(1007) =< aux(104)+1
s(1008) =< aux(104)
s(1009) =< s(1003)*aux(104)
s(1010) =< s(1003)*s(1007)
s(1011) =< s(1003)*s(1008)
s(1012) =< s(1003)*s(1007)
s(1013) =< s(1010)
s(1014) =< s(1011)
s(1015) =< s(1009)
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=1]
#### Cost of chains of fun27(V,V3,V4,Out):
* Chain [53]: 10*s(1029)+6*s(1032)+12*s(1033)+23
Such that:aux(107) =< 1
aux(108) =< V3
aux(109) =< V3+1
s(1029) =< aux(107)
s(1032) =< aux(109)
s(1033) =< aux(108)
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [52]: 11*s(1044)+33*s(1045)+6*s(1047)+12*s(1048)+2*s(1065)+10*s(1066)+8*s(1067)+4*s(1068)+104
Such that:aux(110) =< 1
aux(111) =< 2
aux(112) =< V3
aux(113) =< V3+1
s(1044) =< aux(111)
s(1047) =< aux(113)
s(1048) =< aux(112)
s(1045) =< aux(110)
s(1060) =< aux(110)+1
s(1061) =< aux(110)
s(1062) =< s(1045)*aux(110)
s(1063) =< s(1045)*s(1060)
s(1064) =< s(1045)*s(1061)
s(1065) =< s(1045)*s(1060)
s(1066) =< s(1063)
s(1067) =< s(1064)
s(1068) =< s(1062)
with precondition: [V=0,V4=1,V3+3=Out,V3>=0]
* Chain [51]: 12*s(1070)+33*s(1071)+14*s(1077)+43*s(1079)+37*s(1080)+57*s(1081)+78*s(1083)+12*s(1093)+46*s(1094)+4*s(1100)+20*s(1101)+16*s(1102)+8*s(1103)+30*s(1104)+34*s(1105)+112*s(1106)+8*s(1110)+40*s(1111)+32*s(1112)+16*s(1113)+88*s(1114)+58*s(1115)+4*s(1119)+20*s(1120)+16*s(1121)+8*s(1122)+4*s(1126)+20*s(1127)+16*s(1128)+8*s(1129)+6*s(1131)+12*s(1132)+2*s(1149)+10*s(1150)+8*s(1151)+4*s(1152)+21
Such that:s(1074) =< V4/2
s(1075) =< V4/2+1/2
s(1076) =< 2/3*V4
aux(114) =< V3
aux(115) =< V3+1
aux(116) =< V4
aux(117) =< V4+1
s(1131) =< aux(115)
s(1070) =< aux(117)
s(1132) =< aux(114)
s(1071) =< aux(116)
s(1085) =< aux(116)+1
s(1086) =< aux(116)
s(1146) =< s(1071)*aux(116)
s(1147) =< s(1071)*s(1085)
s(1148) =< s(1071)*s(1086)
s(1149) =< s(1071)*s(1085)
s(1150) =< s(1147)
s(1151) =< s(1148)
s(1152) =< s(1146)
s(1077) =< aux(116)
s(1079) =< aux(117)
s(1080) =< s(1074)
s(1081) =< s(1075)
s(1079) =< s(1075)
s(1082) =< s(1076)
s(1083) =< s(1076)
s(1084) =< aux(116)+2
s(1077) =< s(1070)+aux(116)
s(1082) =< s(1070)* (1/3)+s(1076)
s(1083) =< s(1070)* (1/3)+s(1076)
s(1080) =< s(1070)* (1/2)+s(1074)
s(1083) =< s(1070)* (1/2)+s(1074)
s(1087) =< s(1077)*s(1084)
s(1088) =< s(1077)*s(1085)
s(1089) =< s(1083)*s(1084)
s(1090) =< s(1083)*s(1085)
s(1091) =< s(1080)*s(1085)
s(1092) =< s(1080)*s(1086)
s(1093) =< s(1087)
s(1094) =< s(1088)
s(1095) =< s(1085)+1
s(1096) =< s(1085)
s(1097) =< s(1094)*s(1085)
s(1098) =< s(1094)*s(1095)
s(1099) =< s(1094)*s(1096)
s(1100) =< s(1094)*s(1095)
s(1101) =< s(1098)
s(1102) =< s(1099)
s(1103) =< s(1097)
s(1104) =< s(1082)
s(1105) =< s(1089)
s(1106) =< s(1090)
s(1107) =< s(1106)*s(1085)
s(1108) =< s(1106)*s(1095)
s(1109) =< s(1106)*s(1096)
s(1110) =< s(1106)*s(1095)
s(1111) =< s(1108)
s(1112) =< s(1109)
s(1113) =< s(1107)
s(1114) =< s(1091)
s(1115) =< s(1092)
s(1116) =< s(1115)*aux(116)
s(1117) =< s(1115)*s(1085)
s(1118) =< s(1115)*s(1086)
s(1119) =< s(1115)*s(1085)
s(1120) =< s(1117)
s(1121) =< s(1118)
s(1122) =< s(1116)
s(1123) =< s(1114)*s(1085)
s(1124) =< s(1114)*s(1095)
s(1125) =< s(1114)*s(1096)
s(1126) =< s(1114)*s(1095)
s(1127) =< s(1124)
s(1128) =< s(1125)
s(1129) =< s(1123)
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=2]
#### Cost of chains of fun26(V,V3,V4,Out):
* Chain [59]: 22*s(1154)+31
Such that:aux(119) =< 1
s(1154) =< aux(119)
with precondition: [V=0,V3=0,V4=0,Out=2]
* Chain [58]: 47*s(1169)+13*s(1175)+2*s(1190)+10*s(1191)+8*s(1192)+4*s(1193)+112
Such that:aux(121) =< 1
aux(122) =< 2
s(1169) =< aux(121)
s(1175) =< aux(122)
s(1185) =< aux(121)+1
s(1186) =< aux(121)
s(1187) =< s(1169)*aux(121)
s(1188) =< s(1169)*s(1185)
s(1189) =< s(1169)*s(1186)
s(1190) =< s(1169)*s(1185)
s(1191) =< s(1188)
s(1192) =< s(1189)
s(1193) =< s(1187)
with precondition: [V=0,V3=0,V4=1,Out=3]
* Chain [57]: 10*s(1195)+14*s(1201)+37*s(1202)+2*s(1219)+10*s(1220)+8*s(1221)+4*s(1222)+14*s(1223)+43*s(1224)+37*s(1225)+57*s(1226)+78*s(1228)+12*s(1236)+46*s(1237)+4*s(1243)+20*s(1244)+16*s(1245)+8*s(1246)+30*s(1247)+34*s(1248)+112*s(1249)+8*s(1253)+40*s(1254)+32*s(1255)+16*s(1256)+88*s(1257)+58*s(1258)+4*s(1262)+20*s(1263)+16*s(1264)+8*s(1265)+4*s(1269)+20*s(1270)+16*s(1271)+8*s(1272)+29
Such that:s(1203) =< V4/2
s(1204) =< V4/2+1/2
s(1205) =< 2/3*V4
aux(124) =< 1
aux(125) =< V4
aux(126) =< V4+1
s(1195) =< aux(124)
s(1201) =< aux(126)
s(1202) =< aux(125)
s(1214) =< aux(125)+1
s(1215) =< aux(125)
s(1216) =< s(1202)*aux(125)
s(1217) =< s(1202)*s(1214)
s(1218) =< s(1202)*s(1215)
s(1219) =< s(1202)*s(1214)
s(1220) =< s(1217)
s(1221) =< s(1218)
s(1222) =< s(1216)
s(1223) =< aux(125)
s(1224) =< aux(126)
s(1225) =< s(1203)
s(1226) =< s(1204)
s(1224) =< s(1204)
s(1227) =< s(1205)
s(1228) =< s(1205)
s(1229) =< aux(125)+2
s(1223) =< s(1201)+aux(125)
s(1227) =< s(1201)* (1/3)+s(1205)
s(1228) =< s(1201)* (1/3)+s(1205)
s(1225) =< s(1201)* (1/2)+s(1203)
s(1228) =< s(1201)* (1/2)+s(1203)
s(1230) =< s(1223)*s(1229)
s(1231) =< s(1223)*s(1214)
s(1232) =< s(1228)*s(1229)
s(1233) =< s(1228)*s(1214)
s(1234) =< s(1225)*s(1214)
s(1235) =< s(1225)*s(1215)
s(1236) =< s(1230)
s(1237) =< s(1231)
s(1238) =< s(1214)+1
s(1239) =< s(1214)
s(1240) =< s(1237)*s(1214)
s(1241) =< s(1237)*s(1238)
s(1242) =< s(1237)*s(1239)
s(1243) =< s(1237)*s(1238)
s(1244) =< s(1241)
s(1245) =< s(1242)
s(1246) =< s(1240)
s(1247) =< s(1227)
s(1248) =< s(1232)
s(1249) =< s(1233)
s(1250) =< s(1249)*s(1214)
s(1251) =< s(1249)*s(1238)
s(1252) =< s(1249)*s(1239)
s(1253) =< s(1249)*s(1238)
s(1254) =< s(1251)
s(1255) =< s(1252)
s(1256) =< s(1250)
s(1257) =< s(1234)
s(1258) =< s(1235)
s(1259) =< s(1258)*aux(125)
s(1260) =< s(1258)*s(1214)
s(1261) =< s(1258)*s(1215)
s(1262) =< s(1258)*s(1214)
s(1263) =< s(1260)
s(1264) =< s(1261)
s(1265) =< s(1259)
s(1266) =< s(1257)*s(1214)
s(1267) =< s(1257)*s(1238)
s(1268) =< s(1257)*s(1239)
s(1269) =< s(1257)*s(1238)
s(1270) =< s(1267)
s(1271) =< s(1268)
s(1272) =< s(1266)
with precondition: [V=0,V3=0,V4+2=Out,V4>=2]
* Chain [56]: 11*s(1274)+33*s(1275)+2*s(1284)+10*s(1285)+8*s(1286)+4*s(1287)+12*s(1292)+30
Such that:aux(127) =< 1
aux(128) =< V3
aux(129) =< V3+1
s(1292) =< aux(127)
s(1274) =< aux(129)
s(1275) =< aux(128)
s(1279) =< aux(128)+1
s(1280) =< aux(128)
s(1281) =< s(1275)*aux(128)
s(1282) =< s(1275)*s(1279)
s(1283) =< s(1275)*s(1280)
s(1284) =< s(1275)*s(1279)
s(1285) =< s(1282)
s(1286) =< s(1283)
s(1287) =< s(1281)
with precondition: [V=0,V4=0,V3+2=Out,V3>=1]
* Chain [55]: 11*s(1301)+33*s(1302)+2*s(1311)+10*s(1312)+8*s(1313)+4*s(1314)+13*s(1319)+37*s(1320)+2*s(1334)+10*s(1335)+8*s(1336)+4*s(1337)+111
Such that:aux(130) =< 1
aux(131) =< 2
aux(132) =< V3
aux(133) =< V3+1
s(1319) =< aux(131)
s(1301) =< aux(133)
s(1302) =< aux(132)
s(1320) =< aux(130)
s(1329) =< aux(130)+1
s(1330) =< aux(130)
s(1331) =< s(1320)*aux(130)
s(1332) =< s(1320)*s(1329)
s(1333) =< s(1320)*s(1330)
s(1334) =< s(1320)*s(1329)
s(1335) =< s(1332)
s(1336) =< s(1333)
s(1337) =< s(1331)
s(1306) =< aux(132)+1
s(1307) =< aux(132)
s(1308) =< s(1302)*aux(132)
s(1309) =< s(1302)*s(1306)
s(1310) =< s(1302)*s(1307)
s(1311) =< s(1302)*s(1306)
s(1312) =< s(1309)
s(1313) =< s(1310)
s(1314) =< s(1308)
with precondition: [V=0,V4=1,V3+3=Out,V3>=1]
* Chain [54]: 11*s(1339)+33*s(1340)+2*s(1349)+10*s(1350)+8*s(1351)+4*s(1352)+14*s(1357)+37*s(1358)+2*s(1375)+10*s(1376)+8*s(1377)+4*s(1378)+14*s(1379)+43*s(1380)+37*s(1381)+57*s(1382)+78*s(1384)+12*s(1392)+46*s(1393)+4*s(1399)+20*s(1400)+16*s(1401)+8*s(1402)+30*s(1403)+34*s(1404)+112*s(1405)+8*s(1409)+40*s(1410)+32*s(1411)+16*s(1412)+88*s(1413)+58*s(1414)+4*s(1418)+20*s(1419)+16*s(1420)+8*s(1421)+4*s(1425)+20*s(1426)+16*s(1427)+8*s(1428)+28
Such that:s(1359) =< V4/2
s(1360) =< V4/2+1/2
s(1361) =< 2/3*V4
aux(134) =< V3
aux(135) =< V3+1
aux(136) =< V4
aux(137) =< V4+1
s(1339) =< aux(135)
s(1357) =< aux(137)
s(1340) =< aux(134)
s(1358) =< aux(136)
s(1370) =< aux(136)+1
s(1371) =< aux(136)
s(1372) =< s(1358)*aux(136)
s(1373) =< s(1358)*s(1370)
s(1374) =< s(1358)*s(1371)
s(1375) =< s(1358)*s(1370)
s(1376) =< s(1373)
s(1377) =< s(1374)
s(1378) =< s(1372)
s(1379) =< aux(136)
s(1380) =< aux(137)
s(1381) =< s(1359)
s(1382) =< s(1360)
s(1380) =< s(1360)
s(1383) =< s(1361)
s(1384) =< s(1361)
s(1385) =< aux(136)+2
s(1379) =< s(1357)+aux(136)
s(1383) =< s(1357)* (1/3)+s(1361)
s(1384) =< s(1357)* (1/3)+s(1361)
s(1381) =< s(1357)* (1/2)+s(1359)
s(1384) =< s(1357)* (1/2)+s(1359)
s(1386) =< s(1379)*s(1385)
s(1387) =< s(1379)*s(1370)
s(1388) =< s(1384)*s(1385)
s(1389) =< s(1384)*s(1370)
s(1390) =< s(1381)*s(1370)
s(1391) =< s(1381)*s(1371)
s(1392) =< s(1386)
s(1393) =< s(1387)
s(1394) =< s(1370)+1
s(1395) =< s(1370)
s(1396) =< s(1393)*s(1370)
s(1397) =< s(1393)*s(1394)
s(1398) =< s(1393)*s(1395)
s(1399) =< s(1393)*s(1394)
s(1400) =< s(1397)
s(1401) =< s(1398)
s(1402) =< s(1396)
s(1403) =< s(1383)
s(1404) =< s(1388)
s(1405) =< s(1389)
s(1406) =< s(1405)*s(1370)
s(1407) =< s(1405)*s(1394)
s(1408) =< s(1405)*s(1395)
s(1409) =< s(1405)*s(1394)
s(1410) =< s(1407)
s(1411) =< s(1408)
s(1412) =< s(1406)
s(1413) =< s(1390)
s(1414) =< s(1391)
s(1415) =< s(1414)*aux(136)
s(1416) =< s(1414)*s(1370)
s(1417) =< s(1414)*s(1371)
s(1418) =< s(1414)*s(1370)
s(1419) =< s(1416)
s(1420) =< s(1417)
s(1421) =< s(1415)
s(1422) =< s(1413)*s(1370)
s(1423) =< s(1413)*s(1394)
s(1424) =< s(1413)*s(1395)
s(1425) =< s(1413)*s(1394)
s(1426) =< s(1423)
s(1427) =< s(1424)
s(1428) =< s(1422)
s(1344) =< aux(134)+1
s(1345) =< aux(134)
s(1346) =< s(1340)*aux(134)
s(1347) =< s(1340)*s(1344)
s(1348) =< s(1340)*s(1345)
s(1349) =< s(1340)*s(1344)
s(1350) =< s(1347)
s(1351) =< s(1348)
s(1352) =< s(1346)
with precondition: [V=0,V3+V4+2=Out,V3>=1,V4>=2]
#### Cost of chains of fun30(V,V3,Out):
* Chain [61]: 2*s(1430)+6
Such that:s(1430) =< 1
with precondition: [V=0,V3=0,Out=0]
* Chain [60]: 3*s(1433)+17*s(1434)+2*s(1443)+10*s(1444)+8*s(1445)+4*s(1446)+5
Such that:aux(138) =< V3
aux(139) =< V3+1
s(1433) =< aux(139)
s(1434) =< aux(138)
s(1438) =< aux(138)+1
s(1439) =< aux(138)
s(1440) =< s(1434)*aux(138)
s(1441) =< s(1434)*s(1438)
s(1442) =< s(1434)*s(1439)
s(1443) =< s(1434)*s(1438)
s(1444) =< s(1441)
s(1445) =< s(1442)
s(1446) =< s(1440)
with precondition: [V=0,Out=0,V3>=1]
#### Cost of chains of start(V,V3,V4):
* Chain [62]: 1195*s(1448)+287*s(1490)+50*s(1503)+250*s(1504)+200*s(1505)+100*s(1506)+249*s(1550)+715*s(1551)+46*s(1563)+230*s(1564)+184*s(1565)+92*s(1566)+252*s(1608)+774*s(1610)+666*s(1611)+1026*s(1612)+1404*s(1614)+216*s(1624)+828*s(1625)+72*s(1631)+360*s(1632)+288*s(1633)+144*s(1634)+540*s(1635)+612*s(1636)+2016*s(1637)+144*s(1641)+720*s(1642)+576*s(1643)+288*s(1644)+1584*s(1645)+1044*s(1646)+72*s(1650)+360*s(1651)+288*s(1652)+144*s(1653)+72*s(1657)+360*s(1658)+288*s(1659)+144*s(1660)+229*s(1710)+573*s(1711)+26*s(1720)+130*s(1721)+104*s(1722)+52*s(1723)+196*s(1756)+602*s(1758)+518*s(1759)+798*s(1760)+1092*s(1762)+168*s(1772)+644*s(1773)+56*s(1779)+280*s(1780)+224*s(1781)+112*s(1782)+420*s(1783)+476*s(1784)+1568*s(1785)+112*s(1789)+560*s(1790)+448*s(1791)+224*s(1792)+1232*s(1793)+812*s(1794)+56*s(1798)+280*s(1799)+224*s(1800)+112*s(1801)+56*s(1805)+280*s(1806)+224*s(1807)+112*s(1808)+14*s(4963)+4*s(4964)+43*s(4965)+37*s(4966)+57*s(4967)+78*s(4969)+12*s(4979)+46*s(4980)+4*s(4986)+20*s(4987)+16*s(4988)+8*s(4989)+30*s(4990)+34*s(4991)+112*s(4992)+8*s(4996)+40*s(4997)+32*s(4998)+16*s(4999)+88*s(5000)+58*s(5001)+4*s(5005)+20*s(5006)+16*s(5007)+8*s(5008)+4*s(5012)+20*s(5013)+16*s(5014)+8*s(5015)+17*s(5018)+2*s(5024)+10*s(5025)+8*s(5026)+4*s(5027)+196
Such that:s(4960) =< V/2
s(4961) =< V/2+1/2
s(4962) =< 2/3*V
aux(264) =< 1
aux(265) =< 2
aux(266) =< V
aux(267) =< V+1
aux(268) =< V3
aux(269) =< V3+1
aux(270) =< V3/2
aux(271) =< V3/2+1/2
aux(272) =< 2/3*V3
aux(273) =< V4
aux(274) =< V4+1
aux(275) =< V4/2
aux(276) =< V4/2+1/2
aux(277) =< 2/3*V4
s(1448) =< aux(264)
s(1490) =< aux(265)
s(4964) =< aux(267)
s(1710) =< aux(269)
s(1550) =< aux(274)
s(1498) =< aux(264)+1
s(1499) =< aux(264)
s(1500) =< s(1448)*aux(264)
s(1501) =< s(1448)*s(1498)
s(1502) =< s(1448)*s(1499)
s(1503) =< s(1448)*s(1498)
s(1504) =< s(1501)
s(1505) =< s(1502)
s(1506) =< s(1500)
s(1608) =< aux(273)
s(1610) =< aux(274)
s(1611) =< aux(275)
s(1612) =< aux(276)
s(1610) =< aux(276)
s(1613) =< aux(277)
s(1614) =< aux(277)
s(1615) =< aux(273)+2
s(1558) =< aux(273)+1
s(1559) =< aux(273)
s(1608) =< s(1550)+aux(273)
s(1613) =< s(1550)* (1/3)+aux(277)
s(1614) =< s(1550)* (1/3)+aux(277)
s(1611) =< s(1550)* (1/2)+aux(275)
s(1614) =< s(1550)* (1/2)+aux(275)
s(1618) =< s(1608)*s(1615)
s(1619) =< s(1608)*s(1558)
s(1620) =< s(1614)*s(1615)
s(1621) =< s(1614)*s(1558)
s(1622) =< s(1611)*s(1558)
s(1623) =< s(1611)*s(1559)
s(1624) =< s(1618)
s(1625) =< s(1619)
s(1626) =< s(1558)+1
s(1627) =< s(1558)
s(1628) =< s(1625)*s(1558)
s(1629) =< s(1625)*s(1626)
s(1630) =< s(1625)*s(1627)
s(1631) =< s(1625)*s(1626)
s(1632) =< s(1629)
s(1633) =< s(1630)
s(1634) =< s(1628)
s(1635) =< s(1613)
s(1636) =< s(1620)
s(1637) =< s(1621)
s(1638) =< s(1637)*s(1558)
s(1639) =< s(1637)*s(1626)
s(1640) =< s(1637)*s(1627)
s(1641) =< s(1637)*s(1626)
s(1642) =< s(1639)
s(1643) =< s(1640)
s(1644) =< s(1638)
s(1645) =< s(1622)
s(1646) =< s(1623)
s(1647) =< s(1646)*aux(273)
s(1648) =< s(1646)*s(1558)
s(1649) =< s(1646)*s(1559)
s(1650) =< s(1646)*s(1558)
s(1651) =< s(1648)
s(1652) =< s(1649)
s(1653) =< s(1647)
s(1654) =< s(1645)*s(1558)
s(1655) =< s(1645)*s(1626)
s(1656) =< s(1645)*s(1627)
s(1657) =< s(1645)*s(1626)
s(1658) =< s(1655)
s(1659) =< s(1656)
s(1660) =< s(1654)
s(1551) =< aux(273)
s(1560) =< s(1551)*aux(273)
s(1561) =< s(1551)*s(1558)
s(1562) =< s(1551)*s(1559)
s(1563) =< s(1551)*s(1558)
s(1564) =< s(1561)
s(1565) =< s(1562)
s(1566) =< s(1560)
s(1711) =< aux(268)
s(1715) =< aux(268)+1
s(1716) =< aux(268)
s(1717) =< s(1711)*aux(268)
s(1718) =< s(1711)*s(1715)
s(1719) =< s(1711)*s(1716)
s(1720) =< s(1711)*s(1715)
s(1721) =< s(1718)
s(1722) =< s(1719)
s(1723) =< s(1717)
s(4963) =< aux(266)
s(4965) =< aux(267)
s(4966) =< s(4960)
s(4967) =< s(4961)
s(4965) =< s(4961)
s(4968) =< s(4962)
s(4969) =< s(4962)
s(4970) =< aux(266)+2
s(4971) =< aux(266)+1
s(4972) =< aux(266)
s(4963) =< s(4964)+aux(266)
s(4968) =< s(4964)* (1/3)+s(4962)
s(4969) =< s(4964)* (1/3)+s(4962)
s(4966) =< s(4964)* (1/2)+s(4960)
s(4969) =< s(4964)* (1/2)+s(4960)
s(4973) =< s(4963)*s(4970)
s(4974) =< s(4963)*s(4971)
s(4975) =< s(4969)*s(4970)
s(4976) =< s(4969)*s(4971)
s(4977) =< s(4966)*s(4971)
s(4978) =< s(4966)*s(4972)
s(4979) =< s(4973)
s(4980) =< s(4974)
s(4981) =< s(4971)+1
s(4982) =< s(4971)
s(4983) =< s(4980)*s(4971)
s(4984) =< s(4980)*s(4981)
s(4985) =< s(4980)*s(4982)
s(4986) =< s(4980)*s(4981)
s(4987) =< s(4984)
s(4988) =< s(4985)
s(4989) =< s(4983)
s(4990) =< s(4968)
s(4991) =< s(4975)
s(4992) =< s(4976)
s(4993) =< s(4992)*s(4971)
s(4994) =< s(4992)*s(4981)
s(4995) =< s(4992)*s(4982)
s(4996) =< s(4992)*s(4981)
s(4997) =< s(4994)
s(4998) =< s(4995)
s(4999) =< s(4993)
s(5000) =< s(4977)
s(5001) =< s(4978)
s(5002) =< s(5001)*aux(266)
s(5003) =< s(5001)*s(4971)
s(5004) =< s(5001)*s(4972)
s(5005) =< s(5001)*s(4971)
s(5006) =< s(5003)
s(5007) =< s(5004)
s(5008) =< s(5002)
s(5009) =< s(5000)*s(4971)
s(5010) =< s(5000)*s(4981)
s(5011) =< s(5000)*s(4982)
s(5012) =< s(5000)*s(4981)
s(5013) =< s(5010)
s(5014) =< s(5011)
s(5015) =< s(5009)
s(5018) =< aux(266)
s(5021) =< s(5018)*aux(266)
s(5022) =< s(5018)*s(4971)
s(5023) =< s(5018)*s(4972)
s(5024) =< s(5018)*s(4971)
s(5025) =< s(5022)
s(5026) =< s(5023)
s(5027) =< s(5021)
s(1756) =< aux(268)
s(1758) =< aux(269)
s(1759) =< aux(270)
s(1760) =< aux(271)
s(1758) =< aux(271)
s(1761) =< aux(272)
s(1762) =< aux(272)
s(1763) =< aux(268)+2
s(1756) =< s(1710)+aux(268)
s(1761) =< s(1710)* (1/3)+aux(272)
s(1762) =< s(1710)* (1/3)+aux(272)
s(1759) =< s(1710)* (1/2)+aux(270)
s(1762) =< s(1710)* (1/2)+aux(270)
s(1766) =< s(1756)*s(1763)
s(1767) =< s(1756)*s(1715)
s(1768) =< s(1762)*s(1763)
s(1769) =< s(1762)*s(1715)
s(1770) =< s(1759)*s(1715)
s(1771) =< s(1759)*s(1716)
s(1772) =< s(1766)
s(1773) =< s(1767)
s(1774) =< s(1715)+1
s(1775) =< s(1715)
s(1776) =< s(1773)*s(1715)
s(1777) =< s(1773)*s(1774)
s(1778) =< s(1773)*s(1775)
s(1779) =< s(1773)*s(1774)
s(1780) =< s(1777)
s(1781) =< s(1778)
s(1782) =< s(1776)
s(1783) =< s(1761)
s(1784) =< s(1768)
s(1785) =< s(1769)
s(1786) =< s(1785)*s(1715)
s(1787) =< s(1785)*s(1774)
s(1788) =< s(1785)*s(1775)
s(1789) =< s(1785)*s(1774)
s(1790) =< s(1787)
s(1791) =< s(1788)
s(1792) =< s(1786)
s(1793) =< s(1770)
s(1794) =< s(1771)
s(1795) =< s(1794)*aux(268)
s(1796) =< s(1794)*s(1715)
s(1797) =< s(1794)*s(1716)
s(1798) =< s(1794)*s(1715)
s(1799) =< s(1796)
s(1800) =< s(1797)
s(1801) =< s(1795)
s(1802) =< s(1793)*s(1715)
s(1803) =< s(1793)*s(1774)
s(1804) =< s(1793)*s(1775)
s(1805) =< s(1793)*s(1774)
s(1806) =< s(1803)
s(1807) =< s(1804)
s(1808) =< s(1802)
with precondition: []
Closed-form bounds of start(V,V3,V4):
-------------------------------------
* Chain [62] with precondition: []
- Upper bound: nat(V)*185+2865+nat(V)*202*nat(V)+nat(V)*48*nat(V)*nat(V)+nat(V)*96*nat(V)*nat(2/3*V)+nat(V)*96*nat(V)*nat(V/2)+nat(V)*386*nat(2/3*V)+nat(V)*290*nat(V/2)+nat(V3)*2913+nat(V3)*2804*nat(V3)+nat(V3)*672*nat(V3)*nat(V3)+nat(V3)*1344*nat(V3)*nat(2/3*V3)+nat(V3)*1344*nat(V3)*nat(V3/2)+nat(V3)*5404*nat(2/3*V3)+nat(V3)*4060*nat(V3/2)+nat(V4)*3799+nat(V4)*3756*nat(V4)+nat(V4)*864*nat(V4)*nat(V4)+nat(V4)*1728*nat(V4)*nat(2/3*V4)+nat(V4)*1728*nat(V4)*nat(V4/2)+nat(V4)*6948*nat(2/3*V4)+nat(V4)*5220*nat(V4/2)+nat(2/3*V)*432+nat(2/3*V3)*6048+nat(2/3*V4)*7776+nat(V+1)*47+nat(V3+1)*831+nat(V4+1)*1023+nat(V/2+1/2)*57+nat(V3/2+1/2)*798+nat(V4/2+1/2)*1026+nat(V/2)*197+nat(V3/2)*2758+nat(V4/2)*3546
- Complexity: n^3
### Maximum cost of start(V,V3,V4): nat(V)*185+2865+nat(V)*202*nat(V)+nat(V)*48*nat(V)*nat(V)+nat(V)*96*nat(V)*nat(2/3*V)+nat(V)*96*nat(V)*nat(V/2)+nat(V)*386*nat(2/3*V)+nat(V)*290*nat(V/2)+nat(V3)*2913+nat(V3)*2804*nat(V3)+nat(V3)*672*nat(V3)*nat(V3)+nat(V3)*1344*nat(V3)*nat(2/3*V3)+nat(V3)*1344*nat(V3)*nat(V3/2)+nat(V3)*5404*nat(2/3*V3)+nat(V3)*4060*nat(V3/2)+nat(V4)*3799+nat(V4)*3756*nat(V4)+nat(V4)*864*nat(V4)*nat(V4)+nat(V4)*1728*nat(V4)*nat(2/3*V4)+nat(V4)*1728*nat(V4)*nat(V4/2)+nat(V4)*6948*nat(2/3*V4)+nat(V4)*5220*nat(V4/2)+nat(2/3*V)*432+nat(2/3*V3)*6048+nat(2/3*V4)*7776+nat(V+1)*47+nat(V3+1)*831+nat(V4+1)*1023+nat(V/2+1/2)*57+nat(V3/2+1/2)*798+nat(V4/2+1/2)*1026+nat(V/2)*197+nat(V3/2)*2758+nat(V4/2)*3546
Asymptotic class: n^3
* Total analysis performed in 21572 ms.